A:Type, eq:EqDecider(A), L1, L2:(A List), x:A.
(x  l_intersection(eq;L1;L2))  ((x  L1) & (x  L2)) 

latex

Definitions	x:AB(x), P  Q, P  Q, x:A  B(x), (x  l), P & Q, P  Q, x:A. B(x), b, l_intersection(eq;L1;L2), type List, EqDecider(T), Type
Lemmas	member filter, iff functionality wrt iff, and functionality wrt iff, assert-deq-member